weakPrecondSendR2{$a:ut2, $tg:ut2}
weakPrecondSendR2(T; t; p; l; ds; P; f)
== ([Rpre(source(l);ds;"$a";p;P); 

== ([Rsends(ds;locl("$a");Outcome;l;"$tg" : T;[<"$tg", s,v. [if P(s) then f(s,v) else t fi ]>]);

== ([Rsframe(l;"$tg";[locl("$a")])]) 

latex

---

clarification:

weakPrecondSendR2{$a:ut2, $tg:ut2}
weakPrecondSendR2(T; t; p; l; ds; P; f)
== ([Rpre(source(l);ds;"$a";p;P); 

== ([Rsends(ds;locl("$a");p-outcome(p);l;"$tg" : T;[<"$tg"
== ([Rsends(ds;locl("$a");p-outcome(p);l;"$tg" : T;[, s,v. [if P(s) then f(s,v) else t fi  / []]
== ([Rsends(ds;locl("$a");p-outcome(p);l;"$tg" : T;[> / 
== ([Rsends(ds;locl("$a");p-outcome(p);l;"$tg" : T;[[]]) / 
== ([[Rsframe(l;"$tg";[locl("$a") / []]) / []]]) 

latex

Definitions

(L), Rpre(loc;ds;a;p;P), source(l), Rsends(ds;knd;T;l;dt;g), Outcome, x : v, <a, b>, x.A(x), if b then t else f fi , f(a), Rsframe(lnk;tag;L), [car / cdr], locl(a), "$x", []